|
| creator |
Thoma, Daniel
| | date |
2008
| | | | description |
64 pages
| |
Modelchecking ist ein Verfahren, um Eingenschaften eines Systems zu
verifizieren, indem der Zustandsraum des Systems vollständig
untersucht wird. Für viele reale Systeme, insbesondere für
Softwaresysteme, wird dieser Zustandraum sehr groß. Dies macht die
Analyse des Zustandsraums schnell zu aufwendig, selbst dann, wenn
symbolische Darstellungen verwendet werden, um Systeme und
Zustandsmengen zu repräsentieren.
Um solche Systeme dennoch analysieren zu können, kann vom konkreten
System abstrahiert werden, indem jeweils mehrere, konkrete Zustände
zu einem abstrakten Zustand zusammengefasst werden. Eine Transition
zwischen zwei abstrakten Zuständen ist üblicherweise dann
möglich, wenn eine entsprechende konkrete Transition existiert.
Predicate-Abstraction ist eine Technik um Abstraktionen zu
beschreiben und zu berechnen. Um die Abstraktion zu beschreiben wird
eine Menge von Prädikaten über die Zustandsvariablen eines
konkreten Systems verwendet. Ein abstrakter Zustand legt dann für
jedes Prädikat fest, ob die zugehörigen, konkreten Zustände das
Prädikate erfüllen oder nicht erfüllen müssen. Ein Prädikat
teilt den Zustandsraum in eine Menge von konkreten Zuständen, die
das Prädikat erfüllen, und in eine Menge von Zuständen, die das
Prädikat nicht erfüllen. Die Schnittmengen für alle Prädikate
entsprechen dann den abstrakten Zuständen.
Um die abstrakten Transitionen zu bestimmen, wird mit Hilfe eines
Theorembeweisers überprüft, ob aus den Prädikaten des einen,
abstrakten Zustandes und der Transitionsrelation des Systems folgt,
dass ein konkreter Zustand des anderen, abstrakten Zustandes durch
eine konkrete Transition erreichbar ist.
Auf den so erzeugten, abstrakten Systemen wird dann Modelchecking
durchgeführt. Schlägt die Verifikation der gewünschten
Eigenschaft fehl, wird ein Ablauf im abstrakten System bestimmt, der
die Eigenschaft verletzt. Dann wird zunächst überprüft, ob ein
entsprechender Ablauf auch im konkreten System existiert. Ist dies
nicht der Fall, muss die Abstraktion verbessert werden. Dies wird
üblicherweise erreicht, indem abstrakte Zustände so aufgeteilt
werden, dass der abstrakte Ablauf nicht mehr existiert.
Solche Abstraktionen zeigen mehr Verhalten, als das konkrete System,
d.h. es sind mehr Abläufe möglich, als im konkreten System
tatsächlich auftreten. Aus diesem Grund eignen sich solche
Abstraktionen nicht, um die Existenz von Abläufen zu verifizieren,
es ist lediglich möglich zu überprüfen, dass alle Abläufe
bestimmte Eigenschaften erfüllen. Außerdem kann die Verifikation
einer Eigenschaft fehlschlagen, obwohl sie das konkrete System
erfüllt. Daher ist es notwendig zu überprüfen, ob ein
unzulässiger, abstrakter Ablauf auch tatsächlich einem konkreten
Ablauf entspricht. Um Ausagen über die Exisitenz von Abläufen
machen zu können, muss man so abstrahieren, dass höchstens weniger
Abläufe möglich sind. Man kann jedoch nicht so abstrahieren, dass
beide Fälle abgedeckt sind.
Drei-wertige, abstrakte System unterscheiden zwischen abstrakten
?-Transitionen, für die es lediglich mindestens eine konkrete
Transition gibt, und !-Transitionen, für die es für jeden
konkreten Anfangszustand eine entsprechende Transition gibt. Auf
diesen Systemen ist es möglich, gleichzeitig Eigenschaften von
allen Abläufen und die Existenz von Abläufen zu verifizieren. Wenn
eine Eigenschaft für das abstrakte System nicht gilt, ist es zudem
sicher, dass sie auch für das konkrete System nicht gilt. Schlägt
die Verifikation fehl, so kann das auf ?-Transitionen des abstrakten
Systems zurückgeführt werden und die Abstraktion muss so angepasst
werden, dass diese ?-Transitionen entfallen.
Im Rahmen dieser Arbeit wurde Predicate-Abstraction so angepasst,
dass solche drei-wertigen Systeme zur Abstraktion verwendet werden
können. Außerdem wurde symbolisches Modelchecking auf drei-wertige
Systeme übertragen und um ein Verfahren ergänzt, dass die
?-Transitionen findet, die dazu führen, dass die Verifikation einer
Eigenschaft fehl schlägt. Um diese ?-Transitionen aus dem
abstrakten System zu entfernen, wurde ein
Abstraction-Refinement-Verfahren entwickelt, das entsprechend neue
Prädikate generiert.
Diese Verfahren wurden zudem prototypisch implementiert. Dazu wurden
die Theorembeweiser Yices und Z3 verwendet und eine einfache
Modellierungssprache entworfen.
| | format |
application/pdf
| | 1968802 Bytes | |